Inference at * 2 0 1 3 
Iof proof for Lemma multiply nat wf:

.....upcase..... NILNIL

1. i : 
2. j : 
3. 0 < j
4. ((j - 1)  0 )  (0  (i * (j - 1)))
  (j  0 )  (0  (i * j)) 

latex

 by D 0 

latex

 1: 

 1: 5. j  0 
 1:   0  (i * j)
 2: .....wf..... NILNIL

 2:   (j  0 )  
 .

Definitions	Type, s = t, n * m, n - m, #$n, a < b, , , A  B, x:AB(x), i  j , P  Q, t  T,
Lemmas	le wf, ge wf